package tableaux.rules;

import java.util.Set;

import tableaux.*;
import tableaux.backjumping.DependencyImp;
import tableaux.backjumping.DependencyImpMax;

import entities.Individual;
import entities.concept.*;

public class RuleAnd {

	private Completion dc;
	private AndConcept nextExp;
	private Branching br;

	public RuleAnd(Completion dc) {
		super();
		this.dc = dc;
		this.br = this.dc.getCurrentBranching();
	}

	public boolean isApplicable(Individual n) {
		// List<Concept> unexp = new ArrayList<Concept> ();
		// unexp.addAll(n.getLabels());
		// unexp.removeAll(n.getExpandedLabels());
		// if(unexp.size()<1){
		// return false;
		// }
		// for(Concept c : unexp){
		for (Concept c : n.getLabels()) {
			if (n.getExpandedLabels().contains(c)) {
				continue;
			}
			if (c instanceof AndConcept) {
				AndConcept ac = (AndConcept) c;
				if (!n.getLabels().containsAll(ac.getConceptSet())) {
					this.nextExp = ac;
					// System.err.println("ANd rule selecting: "+ac);
					return true;
				}
			}
		}
		return false;
	}

	public boolean applyRule(Individual n) {
		boolean suc = false;
		Set<Concept> addc = this.nextExp.getConceptSet();
		boolean expadd = n.addExpandedLabels(this.nextExp);
		if (expadd && BranchChanges.getRecordingStatus()) {
			br.getBranchChanges().addToExpandedLabel(n, this.nextExp);
		}

		Set<Integer> anddeps = null;
		if (!Completion.DEP_MAX) {
			anddeps = DependencyImp.getDepSetOfConcept(n, nextExp);
		}
		for (Concept ac : addc) {
			if (n.addLabels(ac)) {
				// add dep set
				if (Completion.DEP_MAX) {
					DependencyImpMax.addDep(n, ac,
							DependencyImpMax.getDepOfConcept(n, nextExp));
				} else {
					DependencyImp.setDep(n, ac, anddeps);
				}
				if (BranchChanges.getRecordingStatus()) {
					br.getBranchChanges().addToLabel(n, ac);
				}
				suc = true;
			}
		}
		return suc;
	}

}
